Iof proof for Lemma decidable equal int seg:
i,j:
, x,y:{i..j
}. Dec(x = y)
by ((((Unfold `decidable` 0)
CollapseTHEN (RepD))
)
CollapseTHENA ((Auto_aux (first_nat 1:n
C) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))
C1:
C1: 1. i :
C1: 2. j :
C1: 3. x : {i..j}
C1: 4. y : {i..j}
C1: (x = y) 
(
(x = y))
C.
T